|
|
Těžké tautologie
Pich, Ján ; Krajíček, Jan (vedoucí práce) ; Pudlák, Pavel (oponent)
Skoumáme nedokazatelnost tvrzení NP$\not\subseteq$P/poly v různých fragmentech aritmetiky. Ta se obvykle dosahuje ukázáním těžkosti výrokových formulí kódujících superpolynomiální spodní odhady pro booleovské obvody. Nejprve prezentujeme několik známých technik a tvrzení. Přirozené důkazy, efektívní interpolaci, KPT větu, iterovatelnost, gadget generátory atd. Pak dokážem několik původních výsledků. Ukážeme nedokazatelnost superpolynomiálních spodních odhadů na booleovské obvody v systémech s efektívní interpolaci (modulo složitostní předpoklad) a v systémech podobajících se stromovým Frege systémům manipulujícím s formulemi, které obsahují jen málo proměnných dokazovaného tvrzení. Tyto výsledky jsou založeny na dokazování těžkosti Nisan-Wigdersonových generátorů v príslušných důkazových systémech.
|
|
|
On the Power of Weak Extensions of V0
Müller, Sebastian Peter ; Krajíček, Jan (vedoucí práce) ; Thapen, Neil (oponent) ; Kolodziejczyk, Leszek (oponent)
Název práce: O síle slabých rozšírení teorie V0 Autor: Sebastian Müller Katedra: Katedra Algebry Vedoucí disertační práce: Prof. RNDr. Jan Krajíček, DrSc., Katedra Algebry. Abstrakt: V predložené disertacní práci zkoumáme sílu slabých fragmentu arit- metiky. Činíme tak jak z modelově-teoretického pohledu, tak z pohledu důkazové složitosti. Pohled skrze teorii modelu naznačuje, že malý iniciální segment libo- volného modelu omezené aritmetiky bude modelem silnější teorie. Jako příklad ukážeme, že každý polylogaritmický řez modelu V0 je modelem VNC. Užitím známé souvislosti mezi fragmenty omezené aritmetiky a dokazatelností v ro- zličných důkazových systémech dokážeme separaci mezi rezolucí a TC0 -Frege systémem na náhodných 3CNF-formulích s jistým poměrem počtu klauzulí vůci počtu proměnných. Zkombinováním obou výsledků dostaneme slabší separační výsledek pro rezoluci a Fregeho důkazové systémy omezené hloubky. Klíčová slova: omezená aritmetika, důkazová složitost, Fregeho důkazový systém, Fregeho důkazový systém omezené hloubky, rezoluce Title: On the Power of Weak Extensions of V0 Author: Sebastian Müller Department: Department of Algebra Supervisor: Prof. RNDr. Jan Krajíček, DrSc., Department of Algebra....
|
|
|
On the Power of Weak Extensions of V0
Müller, Sebastian Peter ; Krajíček, Jan (vedoucí práce) ; Thapen, Neil (oponent) ; Kolodziejczyk, Leszek (oponent)
Název práce: O síle slabých rozšírení teorie V0 Autor: Sebastian Müller Katedra: Katedra Algebry Vedoucí disertační práce: Prof. RNDr. Jan Krajíček, DrSc., Katedra Algebry. Abstrakt: V predložené disertacní práci zkoumáme sílu slabých fragmentu arit- metiky. Činíme tak jak z modelově-teoretického pohledu, tak z pohledu důkazové složitosti. Pohled skrze teorii modelu naznačuje, že malý iniciální segment libo- volného modelu omezené aritmetiky bude modelem silnější teorie. Jako příklad ukážeme, že každý polylogaritmický řez modelu V0 je modelem VNC. Užitím známé souvislosti mezi fragmenty omezené aritmetiky a dokazatelností v ro- zličných důkazových systémech dokážeme separaci mezi rezolucí a TC0 -Frege systémem na náhodných 3CNF-formulích s jistým poměrem počtu klauzulí vůci počtu proměnných. Zkombinováním obou výsledků dostaneme slabší separační výsledek pro rezoluci a Fregeho důkazové systémy omezené hloubky. Klíčová slova: omezená aritmetika, důkazová složitost, Fregeho důkazový systém, Fregeho důkazový systém omezené hloubky, rezoluce Title: On the Power of Weak Extensions of V0 Author: Sebastian Müller Department: Department of Algebra Supervisor: Prof. RNDr. Jan Krajíček, DrSc., Department of Algebra....
|
|
|
Metody odhadů složitosti důkazů ve výrokové logice
Peterová, Alena ; Pudlák, Pavel (vedoucí práce) ; Krajíček, Jan (oponent)
V této práci se věnujeme složitosti důkazových systémů pro výrokovou logiku. Nejprve ukážeme exponenciální dolní odhad na složitost rezoluce přímou aplikací Razborovovy aproximační metody, která byla dosud používána pouze pro odhady na velikost monotónních obvodů. Následně použijeme aproximační metodu i pro nový důkaz exponenciálního dolního odhadu na složitost náhodných rezolučních důkazů. To by mělo mít další využití při separování různých teorií v omezené aritmetice. V obou případech využijeme problém z teorie grafů zvaný Broken Mosquito Screens. Na závěr vyslovíme hypotézu, že aproximační metoda bude mít využití i v silnějších důkazových systémech, jako například Cutting Planes. Powered by TCPDF (www.tcpdf.org)
|
|
|
Těžké tautologie
Pich, Ján ; Krajíček, Jan (vedoucí práce) ; Pudlák, Pavel (oponent)
Skoumáme nedokazatelnost tvrzení NP$\not\subseteq$P/poly v různých fragmentech aritmetiky. Ta se obvykle dosahuje ukázáním těžkosti výrokových formulí kódujících superpolynomiální spodní odhady pro booleovské obvody. Nejprve prezentujeme několik známých technik a tvrzení. Přirozené důkazy, efektívní interpolaci, KPT větu, iterovatelnost, gadget generátory atd. Pak dokážem několik původních výsledků. Ukážeme nedokazatelnost superpolynomiálních spodních odhadů na booleovské obvody v systémech s efektívní interpolaci (modulo složitostní předpoklad) a v systémech podobajících se stromovým Frege systémům manipulujícím s formulemi, které obsahují jen málo proměnných dokazovaného tvrzení. Tyto výsledky jsou založeny na dokazování těžkosti Nisan-Wigdersonových generátorů v príslušných důkazových systémech.
|
host ::
RSS.